|
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first-order language of classical set theory, and although of course the logic is constructive, there is no explicit use of constructive types. Rather, there are just sets, thus it can look very much like classical mathematics done on the most common foundations, namely the Zermelo–Fraenkel axioms (ZFC). == Intuitionistic Zermelo–Fraenkel == In 1973, John Myhill proposed a system of set theory based on intuitionistic logic〔Myhill, '' "Some properties of Intuitionistic Zermelo-Fraenkel set theory"'', Proceedings of the 1971 Cambridge Summer School in Mathematical Logic (Lecture Notes in Mathematics 337) (1973) pp 206-231〕 taking the most common foundation, ZFC, and throwing away the axiom of choice (AC) and the law of the excluded middle (LEM), leaving everything else as is. However, different forms of some of the ZFC axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply LEM. The system, which has come to be known as IZF, or Intuitionistic Zermelo–Fraenkel (ZF refers to ZFC without the axiom of choice), has the usual axioms of extensionality, pairing, union, infinity, separation and power set. The axiom of regularity is stated in the form of an axiom schema of set induction. Also, while Myhill used the axiom schema of replacement in his system, IZF usually stands for the version with collection While the axiom of replacement requires the relation ''φ'' to be a function over the set ''A'' (that is, for every ''x'' in ''A'' there is associated exactly one ''y''), the axiom of collection does not: it merely requires there be associated at least one ''y'', and it asserts the existence of a set which collects at least one such ''y'' for each such ''x''. The axiom of regularity as it is normally stated implies LEM, whereas the form of set induction does not. The formal statements of these two schemata are: Adding LEM back to IZF results in ZF, as LEM makes collection equivalent to replacement and set induction equivalent to regularity. Even without LEM, IZF's proof-theoretical power equals that of ZF. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Constructive set theory」の詳細全文を読む スポンサード リンク
|